home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 1.iso / ARGONET / PD / PROGRAMMING / LCLINT2.SPK / test / test_b / lcl / modtest next >
Text File  |  1996-08-28  |  335b  |  21 lines
  1. int x, y;
  2. int ai[];
  3. int bi[];
  4. typedef struct _ts { int a; int b; } tst;
  5. tst ts;
  6. tst *tstp ;
  7.  
  8. int f (int i[], int *j) int ai[]; int x, y; tst ts; tst* tstp; 
  9. {
  10.   let elt be ai[6];
  11.   modifies elt, x, ai[3], ai[3+6], ai[x'], ts.a, tstp'->a, ts;
  12.   ensures true;
  13. }
  14.  
  15. int g (int a[], int *p) int x, y;
  16. {
  17.    modifies x, y;
  18.    ensures true;
  19. }
  20.  
  21.